package com.shigi.sat.structure;

/**
 * Created by Miroslav Šiagi on 27/01/15.
 */
public class SatInstance {
    public final String id;
    private final int numOfLiterals;
    private final int numOfClausules;
    private final int numOfVariables;

    public boolean[] variablesValues;
    public int[] variablesWeights;
    public final SatClausule[] satClausules;

    public boolean evaluatedValue;
    public int numberOfTrueClauses ;

    public SatInstance(String id, int numOfLiterals, int numOfClausules, int numOfVariables) {
        this.id = id;
        this.numOfLiterals = numOfLiterals;
        this.numOfClausules = numOfClausules;
        this.numOfVariables = numOfVariables;
        this.satClausules = new SatClausule[this.numOfClausules];

        for (int i = 0; i < numOfClausules; i++) {
            this.satClausules[i] = new SatClausule(this.numOfLiterals, this);
        }

        this.variablesValues = new boolean[this.numOfVariables];
        this.variablesWeights = new int[this.numOfVariables];
    }

    public SatInstance(SatInstance anotherInstance) {
        this.id = anotherInstance.id;
        this.numOfLiterals = anotherInstance.numOfLiterals;
        this.numOfClausules = anotherInstance.numOfClausules;
        this.numOfVariables = anotherInstance.numOfVariables;
        this.evaluatedValue = anotherInstance.evaluatedValue;
        this.numberOfTrueClauses = anotherInstance.numberOfTrueClauses;

        this.satClausules = new SatClausule[this.numOfClausules];

        for (int i = 0; i < numOfClausules; i++) {
            this.satClausules[i] = new SatClausule(anotherInstance.satClausules[i], this);
        }

        this.variablesValues = new boolean[numOfVariables];
        for (int i = 0; i < numOfVariables; i++) {
            this.variablesValues[i] = anotherInstance.variablesValues[i];
        }

        this.variablesWeights = new int[numOfVariables];
        for (int i = 0; i < numOfVariables; i++) {
            this.variablesWeights[i] = anotherInstance.variablesWeights[i];
        }
    }

    public boolean evaluateClauses() {
        boolean evaluationValue = true;
        for (int i = 0; i < this.numOfClausules && evaluationValue; i++) {
            evaluationValue = evaluationValue && this.satClausules[i].evaluateLiterals();
        }

        this.evaluatedValue = evaluationValue;
        return evaluationValue;
    }


    public int getNumOfLiterals() {
        return numOfLiterals;
    }

    public int getNumOfClausules() {
        return numOfClausules;
    }

    public int getNumOfVariables() {return numOfVariables;}
}
